/**
 *  TiniSatJ :: A Java implemented SAT Solver based on Tinisat 0.22
 *
 *  Copyright (C) 2007 KITAGAWA, Satoshi.
 *
 *  Original TiniSat is available from
 *  http://users.rsise.anu.edu.au/~jinbo/tinisat/
 *
 *  This program is free software; you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License as published by
 *  the Free Software Foundation; either version 2 of the License, or
 *  (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 */

package com.googlecode.tinisat_j;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Comparator;
import org.apache.commons.collections.primitives.ArrayIntList;

interface RestartSterategy {
	int next();
}

class Luby implements RestartSterategy {
    ArrayIntList seq;
    int index;
    int k;

    public Luby() {
        seq = new ArrayIntList(128);
        index = 0;
        k = 1;
    }

    public int next() {
        if (++index == (1 << k) - 1) {
            seq.add(1 << (k++ - 1));
        }
        else {
            seq.add(seq.get(index - (1 << (k - 1))));
        }
        return seq.get(seq.size()-1);
    }
}

public class SatSolver extends CnfManager {
    public static final int HALFLIFE = 128;
    public static final int DT_ = 32;

    int nVars;
    RestartSterategy luby;
    int lubyUnit;
    int nextDecay;
    int nextRestart;

    public SatSolver(Cnf cnf) {
        super(cnf);
        luby = new Luby();
        nextRestart = luby.next() * (lubyUnit = 512);
        nextDecay = HALFLIFE;

        if (dLevel == 0) return;

        for (int i = 1; i<= vc; i++) if (vars[i].value == Var.FREE) {
            if (vars[i].activity[Var.POSI] == 0 && vars[i].activity[Var.NEGA] > 0)
                assertLiteral(-i, null);
            else if (vars[i].activity[Var.NEGA] == 0 && vars[i].activity[Var.POSI] > 0)
                assertLiteral(i, null);
        }

        // initialize variable ordering.
        nVars = 0;
        ArrayList<Var> initialOrder = new ArrayList<Var>();
        for (int i=1; i<= vc; i++) {
            Var var = vars[i];
            if (var.value == Var.FREE && SCORE(i) > 0) {
                initialOrder.add(var); nVars++;
                var.phase = (var.activity[Var.POSI] > var.activity[Var.NEGA]) ? Var.POSI : Var.NEGA;
            }
        }

        Collections.sort(initialOrder, new Comparator<Var>() {

            public int compare(Var v1, Var v2) {
                double d = v2.score() - v1.score();
                if (d < 0) return -1;
                else if (d == 0) return 1;
                else return 1;
            }
        });

        for (int i=0; i< nVars; i++) {
            int id = initialOrder.get(i).id;
            varOrder[i] = id;
            varPosition[id] = i;
        }
        nextVar = 0;
        nextClause = clauses.size() - 1;
    }

    public int selectLiteral() {
        int x = 0;

        int lastClause = nextClause > 256 ? (nextClause - 256) : 0;
        for (int i = nextClause; i >= lastClause; i--) {
            int[] p = clauses.get(nextClause = i);

            boolean sat = false;

            int lit;
            for (int j=0; (lit = p[j]) != 0 && !SET(lit); j++) {
                sat = true;
                break;
            }
            if (sat) continue;

            int score = -1;
            p = clauses.get(i);
            for (int j=0; (lit = p[j]) != 0; j++) {
                if (FREE(lit) && SCORE(Var.VAR(lit)) > score) {
                    x = Var.VAR(lit);
                    score = SCORE(x);
                }
            }

            int d = vars[x].activity[Var.POSI] - vars[x].activity[Var.NEGA];
            if (d > DT_) return x;
            else if (-d > DT_) return -x;
            else return (vars[x].phase == Var.NEGA) ? (-x) : (x);
        }

        for (int i = nextVar; i < nVars; i++) {
            if (vars[varOrder[i]].value == Var.FREE) {
                x = varOrder[i];
                nextVar = i + 1;

                int d = vars[x].activity[Var.POSI] - vars[x].activity[Var.NEGA];
                if (d > DT_) return x;
                else if (-d > DT_) return (-x);
                else return (vars[x].phase == Var.NEGA) ? (-x) : (x);
            }
        }
        return 0;
    }

    public boolean run() {
        if (dLevel == 0) return false;
        for (int lit; (lit = selectLiteral()) != 0;) {
            if (!decide(lit)) do {
                if (aLevel == 0) {
                    verifySolution();
                    return false;
                }

                if (nConflicts == nextDecay) {
                    nextDecay += HALFLIFE;
                    scoreDecay();
                }

                nextClause = clauses.size() - 1;

                if (nConflicts == nextRestart) {
                    nRestarts++;
                    nextRestart += luby.next() * lubyUnit;
                    backtrack(1);
                    if(dLevel != aLevel) break;
                }
                else backtrack(aLevel);
            } while(!assertCL());
        }
        if (!verifySolution()) { System.out.println("s UNKNOWN"); System.exit(0); };
        return true;
    }

    public boolean verifySolution() {
        int lit;

        for (int[] clause: litPools) {
            boolean satisfied = false;
            for(int i=0; (lit = clause[i]) != 0; i++) {
                if(SET(lit)){
                    satisfied = true;
                    break;
                }
            }
            if(!satisfied) return false;
        }
        return true;
    }

    public void printSolution() {
        for(int i = 1; i <= vc; i++) {
            if(vars[i].value == Var.POSI) System.out.print(i + " ");
            else if(vars[i].value == Var.NEGA) System.out.print("-" + i + " ");
        }
        System.out.println("0\n");
    }

    public void printStats(){
        String str = "c " + nDecisions + " decisions, " + nConflicts + " conflicts, " + nRestarts + " restarts";
        System.out.println(str);
        }
}
